\begin{nusmvCommand} {check\_invar} {Performs model checking of invariants}
 
 \cmdLine{check\_invar [-h] [-m | -o output-file] [-n number | -p
 \linebreak "\invarexpr [IN context]"]}
 
Performs invariant checking on the given model. An invariant is a set
of states. Checking the invariant is the process of determining that
all states reachable from the initial states lie in the invariant.
Invariants to be verified can be provided as simple formulas (without
any temporal operators) in the input file via the \code{INVARSPEC}
keyword or directly at command line, using the option \commandopt{p}.
   
Option \commandopt{n} can be used for checking a particular invariant
of the model. If neither \commandopt{n} nor \commandopt{p} are used,
all the invariants are checked.
  
During checking of invariants all the fairness conditions associated
with the model are ignored.
  
If an invariant does not hold, a proof of failure is demonstrated.
This consists of a path starting from an initial state to a state
lying outside the invariant. This path has the property that it is the
shortest path leading to a state outside the invariant.

\begin{cmdOpt}

\opt{-m}{Pipes the output generated by the program in processing
  \code{INVARSPEC}s to the program specified by the \shellvar{PAGER}
  shell variable if defined, else through the \unix command
\shellcommand{more}.}
 
\opt{-o \parameter{\filename{output-file}}}{Writes the output
  generated by the command in processing \code{INVARSPEC}s to the file
  \filename{output-file}.}
            
\opt{-p \parameter{"\invarexpr [IN context]"}}{The command line
  specified invariant formula to be verified.  \code{context} is the
  module instance name which the variables in  \invarexpr must be
  evaluated in.}

\end{cmdOpt}

\end{nusmvCommand}
